Use ordered set to track declared macros, avoid double-declarations#807
Use ordered set to track declared macros, avoid double-declarations#807marcoeilers wants to merge 1 commit intomasterfrom
Conversation
| for (m <- macros) { | ||
| if (!_declaredFreshMacros.contains(m)) | ||
| prover.declare(m) | ||
| } |
There was a problem hiding this comment.
I am bit afraid that using InsertionOrderedSet may hurt performance quite a lot. From what I gathered, this data structure is very inneficient and this may hurt us if the lists are very big.
I wonder if we really are making use of the fact that _declaredFreshMacros only stores once each value. If that is not necessary, could we keep the implementation using a vector and keep this check? ((!_declaredFreshMacros.contains(m)))
There was a problem hiding this comment.
I'm not sure the Vectors will do much better; checking many times if a vector contains a specific value isn't going to be efficient either, right. We just need a good InsertionOrderedSet implementation. But I made a PR for now to just add perform the check.
2 participants
No description provided.